COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	@make(letterhead,Phone"497-4430",Who"John McCarthy",Logo,old,Department csd)
C00007 ENDMK
C⊗;
@make(letterhead,Phone"497-4430",Who"John McCarthy",Logo,old,Department csd)
@style(indent 8)
@blankspace(8 lines)
@begin(address)
Dr. Charles Bachman
Cullinane Data Base Systems
400 Bluehill Drive
Westwood, MA  02090.
@end(address)
@greeting(Dear Dr. Bachman:)
@begin(body)
	This is to recommend Robert S. Boyer and J Strother 
Moore of the University of Texas for the 1982 A. M. Turing award.

	The recommendation is based on the line of research
culminating in their book "A Logic of Computation" published by
the ACM.  It was extended in their "Meta-functions: proving them correct
and using them as new proof procedures" and in their
"A Verification Generator for Fortran".

	Many people, including me, have worked on
methods for proving assertions about computer programs.  What
distinguishes their work and makes it a contribution worthy of
the Turing award is its combination of mathematical clarity,
heuristic ingenuity and demonstrated success as a tool in proving
a wide variety of correctness assertions about a wide variety of
rather substantial programs.

	In particular, they are the first to make a theorem prover
that uses mathematical induction with consistent success.  Most
verification-oriented theorem proving programs don't use induction
themselves at all but rely on mathematical "lemmas" supplied by the
user and then only prove partial correctness.  The Boyer and Moore
success in using induction relies on a very general induction
principle that provides particular schemas oriented towards particular
sentences to be proved.

	Their work is novel in the following respects:

	1. Before it accepts a recursive program, their program requires
information enabling a proof that it defines a total function, i.e. that
it terminates for all combinations of arguments.  This excludes proving
assertions about partial functions such as interpreters, but it leaves
the theorem with a tractable domain with well-defined mathematical
properties.

	2. They have restricted themselves to assertions without
quantifiers except implicit universal quantifiers.  However, they
have shown how assertions that many computer scientists thought required
manipulation of quantifiers for their proofs can be done without
quantifiers.
@newpage
	3. They have a powerful system for deciding what instances
schemas of mathematical induction to use for the particular problem.

	4. They avoid combinatorial explosion by discarding equalities
after they have been used.

	In my opinion, giving them the award will reward first class
work and will inspire other computer scientists to produce program
verification systems that are both practical and theoretically
sound.
@end(body)
Sincerely,




John McCarthy
Professor of Computer Science